Search for: All records

In this paper, we examine the high-probability finite-time theoretical guarantees of the least squares method for system identification of switched linear systems with process noise and without control input. We consider two scenarios: one in which the switching is i.i.d., and the other in which the switching is according to a Markov process. We provide concentration inequalities using a martingale-type argument to bound the identification error at each mode, and we use concentration lemmas for the switching signal. Our bound is in terms of state dimension, trajectory length, finite-time gramian, and properties of the switching signal distribution. We then provide simulations to demonstrate the accuracy of the identification. Additionally, we show that the empirical convergence rate is consistent with our theoretical bound. 

We present a scalable methodology to verify stochastic hybrid systems for inequality linear temporal logic (iLTL) or inequality metric interval temporal logic (iMITL). Using the Mori–Zwanzig reduction method, we construct a finite-state Markov chain reduction of a given stochastic hybrid system and prove that this reduced Markov chain is approximately equivalent to the original system in a distributional sense. Approximate equivalence of the stochastic hybrid system and its Markov chain reduction means that analyzing the Markov chain with respect to a suitably strengthened property allows us to conclude whether the original stochastic hybrid system meets its temporal logic specifications. Based on this, we propose the first statistical model checking algorithms to verify stochastic hybrid systems against correctness properties, expressed in iLTL or iMITL. The scalability of the proposed algorithms is demonstrated by a case study.